(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 69))
(assert (let ((e1(_ bv12162580238593954092817819199619 105)))
(let ((e2(_ bv11064742 24)))
(let ((e3 (bvadd ((_ sign_extend 45) e2) v0)))
(let ((e4 (bvadd ((_ sign_extend 45) e2) v0)))
(let ((e5 (bvlshr e4 e3)))
(let ((e6 ((_ rotate_right 63) v0)))
(let ((e7 (bvashr e6 e6)))
(let ((e8 (ite (bvsgt e4 e3) (_ bv1 1) (_ bv0 1))))
(let ((e9 (bvxnor e3 e6)))
(let ((e10 (bvnot e9)))
(let ((e11 (bvmul e6 e6)))
(let ((e12 ((_ zero_extend 39) e7)))
(let ((e13 (ite (distinct e11 e4) (_ bv1 1) (_ bv0 1))))
(let ((e14 (ite (bvsge e10 ((_ sign_extend 45) e2)) (_ bv1 1) (_ bv0 1))))
(let ((e15 (bvadd e11 ((_ zero_extend 45) e2))))
(let ((e16 (bvadd e11 e7)))
(let ((e17 (ite (distinct v0 v0) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (distinct e9 e6) (_ bv1 1) (_ bv0 1))))
(let ((e19 (bvand e16 e10)))
(let ((e20 ((_ repeat 1) e5)))
(let ((e21 (bvneg e3)))
(let ((e22 (ite (bvsge e11 ((_ zero_extend 68) e18)) (_ bv1 1) (_ bv0 1))))
(let ((e23 (bvudiv ((_ sign_extend 39) e20) e12)))
(let ((e24 (ite (bvuge e9 ((_ sign_extend 68) e8)) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvsub ((_ zero_extend 68) e17) e9)))
(let ((e26 (bvxor e6 e3)))
(let ((e27 ((_ rotate_left 73) e23)))
(let ((e28 (bvlshr e5 v0)))
(let ((e29 (ite (bvsge e5 ((_ zero_extend 45) e2)) (_ bv1 1) (_ bv0 1))))
(let ((e30 (bvor e19 e7)))
(let ((e31 (ite (bvslt e22 e22) (_ bv1 1) (_ bv0 1))))
(let ((e32 (ite (bvslt e25 ((_ zero_extend 68) e24)) (_ bv1 1) (_ bv0 1))))
(let ((e33 (bvshl e32 e17)))
(let ((e34 (bvurem e3 e25)))
(let ((e35 (ite (bvsge e27 ((_ sign_extend 107) e31)) (_ bv1 1) (_ bv0 1))))
(let ((e36 (bvnot e14)))
(let ((e37 (ite (bvule ((_ sign_extend 68) e32) e4) (_ bv1 1) (_ bv0 1))))
(let ((e38 ((_ rotate_left 0) e17)))
(let ((e39 (bvurem e38 e35)))
(let ((e40 (ite (bvult e19 e10) (_ bv1 1) (_ bv0 1))))
(let ((e41 (bvsdiv ((_ sign_extend 68) e18) e7)))
(let ((e42 (bvcomp ((_ zero_extend 36) e7) e1)))
(let ((e43 (bvsle e16 e30)))
(let ((e44 (bvsge e19 v0)))
(let ((e45 (bvslt ((_ sign_extend 36) e5) e1)))
(let ((e46 (bvslt e22 e8)))
(let ((e47 (bvsge ((_ sign_extend 36) e28) e1)))
(let ((e48 (bvule ((_ zero_extend 68) e24) e21)))
(let ((e49 (distinct e25 e41)))
(let ((e50 (bvsle ((_ sign_extend 39) e11) e27)))
(let ((e51 (distinct e30 ((_ sign_extend 68) e13))))
(let ((e52 (= ((_ zero_extend 39) e5) e12)))
(let ((e53 (bvult e34 e19)))
(let ((e54 (bvugt ((_ zero_extend 68) e22) e16)))
(let ((e55 (bvsle ((_ sign_extend 68) e38) e26)))
(let ((e56 (bvsge e7 e26)))
(let ((e57 (bvule ((_ zero_extend 107) e22) e23)))
(let ((e58 (bvult e10 e3)))
(let ((e59 (bvsle e4 e41)))
(let ((e60 (bvsgt e10 ((_ zero_extend 68) e24))))
(let ((e61 (distinct e11 ((_ zero_extend 68) e14))))
(let ((e62 (bvugt e38 e40)))
(let ((e63 (bvsge e30 e25)))
(let ((e64 (bvslt e27 ((_ sign_extend 107) e22))))
(let ((e65 (= e25 ((_ zero_extend 68) e22))))
(let ((e66 (bvsle e4 e3)))
(let ((e67 (bvule e11 e20)))
(let ((e68 (distinct e4 e4)))
(let ((e69 (bvule ((_ sign_extend 39) e28) e23)))
(let ((e70 (bvsgt e28 ((_ zero_extend 68) e22))))
(let ((e71 (bvugt ((_ zero_extend 39) e11) e12)))
(let ((e72 (bvugt ((_ zero_extend 68) e35) e15)))
(let ((e73 (bvsge e35 e40)))
(let ((e74 (bvult ((_ sign_extend 36) e26) e1)))
(let ((e75 (distinct e37 e29)))
(let ((e76 (distinct e41 e34)))
(let ((e77 (bvule e34 e6)))
(let ((e78 (bvuge e7 v0)))
(let ((e79 (bvugt e29 e42)))
(let ((e80 (bvsle e34 e20)))
(let ((e81 (bvuge e23 ((_ zero_extend 39) e26))))
(let ((e82 (distinct e3 e20)))
(let ((e83 (bvult e30 e16)))
(let ((e84 (bvsge e7 e25)))
(let ((e85 (bvsgt e32 e31)))
(let ((e86 (bvuge e17 e32)))
(let ((e87 (bvsle e40 e42)))
(let ((e88 (bvsgt ((_ zero_extend 68) e32) e9)))
(let ((e89 (bvule ((_ sign_extend 68) e33) e6)))
(let ((e90 (bvule e38 e38)))
(let ((e91 (= e20 v0)))
(let ((e92 (bvsgt e7 ((_ zero_extend 68) e31))))
(let ((e93 (bvslt ((_ zero_extend 68) e14) e28)))
(let ((e94 (bvugt ((_ zero_extend 68) e13) e9)))
(let ((e95 (bvugt e39 e36)))
(let ((e96 (bvult e9 ((_ zero_extend 68) e31))))
(let ((e97 (bvsle e3 ((_ sign_extend 68) e14))))
(let ((e98 (bvsge ((_ zero_extend 68) e8) e16)))
(let ((e99 (bvslt e26 ((_ sign_extend 68) e8))))
(let ((e100 (bvslt e26 ((_ zero_extend 68) e8))))
(let ((e101 (bvsle ((_ zero_extend 68) e17) e3)))
(let ((e102 (bvsle e30 ((_ zero_extend 68) e14))))
(let ((e103 (bvuge ((_ sign_extend 39) e4) e23)))
(let ((e104 (bvult e41 ((_ sign_extend 68) e29))))
(let ((e105 (distinct e13 e24)))
(let ((e106 (bvsgt ((_ zero_extend 68) e14) e26)))
(let ((e107 (bvuge e6 e10)))
(let ((e108 (bvugt e4 ((_ sign_extend 68) e32))))
(let ((e109 (= e34 e5)))
(let ((e110 (bvsle e9 e10)))
(let ((e111 (bvuge e19 ((_ zero_extend 68) e17))))
(let ((e112 (bvsge e3 ((_ zero_extend 68) e22))))
(let ((e113 (bvsle ((_ sign_extend 39) e25) e27)))
(let ((e114 (bvslt e35 e39)))
(let ((e115 (bvult e9 e10)))
(let ((e116 (bvsge ((_ sign_extend 68) e17) e28)))
(let ((e117 (distinct e20 e10)))
(let ((e118 (bvuge e11 e41)))
(let ((e119 (distinct ((_ zero_extend 68) e39) e5)))
(let ((e120 (bvsge ((_ zero_extend 45) e2) e19)))
(let ((e121 (bvugt e34 e16)))
(let ((e122 (bvugt ((_ sign_extend 68) e8) e6)))
(let ((e123 (bvule e6 e20)))
(let ((e124 (bvuge ((_ zero_extend 104) e14) e1)))
(let ((e125 (bvsle ((_ sign_extend 68) e37) e5)))
(let ((e126 (bvuge v0 ((_ zero_extend 68) e22))))
(let ((e127 (bvsge ((_ sign_extend 68) e37) e30)))
(let ((e128 (= e17 e33)))
(let ((e129 (bvule ((_ sign_extend 68) e35) e41)))
(let ((e130 (bvult ((_ zero_extend 68) e17) e11)))
(let ((e131 (bvuge ((_ zero_extend 39) e21) e23)))
(let ((e132 (bvuge e11 ((_ sign_extend 68) e38))))
(let ((e133 (bvule ((_ zero_extend 68) e18) e9)))
(let ((e134 (ite e102 e44 e111)))
(let ((e135 (ite e88 e106 e110)))
(let ((e136 (ite e85 e71 e81)))
(let ((e137 (= e84 e62)))
(let ((e138 (= e47 e63)))
(let ((e139 (or e97 e107)))
(let ((e140 (xor e137 e131)))
(let ((e141 (not e122)))
(let ((e142 (xor e124 e117)))
(let ((e143 (= e57 e83)))
(let ((e144 (=> e79 e136)))
(let ((e145 (= e94 e104)))
(let ((e146 (xor e121 e130)))
(let ((e147 (= e59 e112)))
(let ((e148 (= e101 e141)))
(let ((e149 (and e54 e65)))
(let ((e150 (xor e43 e74)))
(let ((e151 (and e100 e92)))
(let ((e152 (not e143)))
(let ((e153 (xor e146 e70)))
(let ((e154 (xor e149 e153)))
(let ((e155 (=> e76 e89)))
(let ((e156 (xor e99 e147)))
(let ((e157 (not e152)))
(let ((e158 (= e125 e61)))
(let ((e159 (ite e98 e82 e98)))
(let ((e160 (xor e119 e119)))
(let ((e161 (xor e150 e55)))
(let ((e162 (and e118 e148)))
(let ((e163 (= e96 e129)))
(let ((e164 (or e68 e157)))
(let ((e165 (ite e72 e66 e142)))
(let ((e166 (or e164 e138)))
(let ((e167 (not e145)))
(let ((e168 (ite e80 e67 e156)))
(let ((e169 (=> e132 e87)))
(let ((e170 (= e93 e113)))
(let ((e171 (xor e128 e168)))
(let ((e172 (not e134)))
(let ((e173 (and e162 e49)))
(let ((e174 (=> e105 e52)))
(let ((e175 (and e159 e133)))
(let ((e176 (and e77 e108)))
(let ((e177 (= e155 e127)))
(let ((e178 (=> e51 e160)))
(let ((e179 (not e69)))
(let ((e180 (or e115 e114)))
(let ((e181 (=> e176 e171)))
(let ((e182 (= e45 e45)))
(let ((e183 (xor e103 e170)))
(let ((e184 (xor e163 e154)))
(let ((e185 (and e182 e60)))
(let ((e186 (not e167)))
(let ((e187 (xor e174 e78)))
(let ((e188 (= e166 e109)))
(let ((e189 (xor e120 e91)))
(let ((e190 (xor e158 e46)))
(let ((e191 (or e172 e165)))
(let ((e192 (=> e135 e187)))
(let ((e193 (ite e188 e139 e180)))
(let ((e194 (and e48 e190)))
(let ((e195 (xor e191 e144)))
(let ((e196 (and e178 e194)))
(let ((e197 (=> e175 e196)))
(let ((e198 (and e140 e181)))
(let ((e199 (ite e50 e183 e183)))
(let ((e200 (not e169)))
(let ((e201 (xor e53 e123)))
(let ((e202 (not e179)))
(let ((e203 (=> e200 e151)))
(let ((e204 (xor e73 e199)))
(let ((e205 (=> e184 e193)))
(let ((e206 (ite e198 e197 e161)))
(let ((e207 (or e202 e90)))
(let ((e208 (=> e173 e56)))
(let ((e209 (not e207)))
(let ((e210 (= e185 e206)))
(let ((e211 (and e203 e189)))
(let ((e212 (or e205 e116)))
(let ((e213 (not e58)))
(let ((e214 (= e186 e195)))
(let ((e215 (and e86 e204)))
(let ((e216 (ite e192 e75 e214)))
(let ((e217 (ite e211 e201 e201)))
(let ((e218 (=> e216 e212)))
(let ((e219 (ite e126 e218 e209)))
(let ((e220 (and e64 e219)))
(let ((e221 (xor e220 e210)))
(let ((e222 (xor e177 e221)))
(let ((e223 (= e222 e222)))
(let ((e224 (or e223 e223)))
(let ((e225 (or e224 e95)))
(let ((e226 (and e213 e208)))
(let ((e227 (=> e217 e225)))
(let ((e228 (not e227)))
(let ((e229 (ite e228 e226 e215)))
(let ((e230 (and e229 (not (= e12 (_ bv0 108))))))
(let ((e231 (and e230 (not (= e25 (_ bv0 69))))))
(let ((e232 (and e231 (not (= e7 (_ bv0 69))))))
(let ((e233 (and e232 (not (= e7 (bvnot (_ bv0 69)))))))
(let ((e234 (and e233 (not (= e35 (_ bv0 1))))))
e234
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
